(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 4.
The certificate found is represented by the following graph.
Start state: 538
Accept states: [539, 540, 541]
Transitions:
538→539[v_1|0]
538→540[w_1|0]
538→541[p_1|0]
538→538[s_1|0, 0_1|0]
538→542[s_1|1]
538→561[s_1|1]
538→580[s_1|1]
538→591[s_1|1]
538→609[s_1|1]
538→544[s_1|2]
538→611[s_1|2]
538→546[s_1|2]
538→565[s_1|2]
538→550[w_1|2]
538→618[s_1|3]
538→637[s_1|2]
538→620[s_1|4]
538→639[s_1|2, s_1|3]
538→622[s_1|4]
538→641[s_1|3, s_1|2]
538→626[w_1|4]
538→645[w_1|3, w_1|2]
542→543[p_1|1]
543→544[s_1|1]
543→546[s_1|2]
543→550[w_1|2]
544→545[p_1|1]
545→546[s_1|1]
545→550[w_1|2]
546→547[s_1|1]
546→549[p_1|2]
547→548[p_1|1]
548→549[p_1|1]
549→550[w_1|1]
550→551[s_1|1]
551→552[s_1|1]
552→553[s_1|1]
553→554[s_1|1]
554→555[s_1|1]
555→556[s_1|1]
556→557[s_1|1]
556→539[s_1|2]
557→558[s_1|1]
557→560[p_1|2]
558→559[p_1|1]
559→560[p_1|1]
560→539[s_1|1]
561→562[s_1|1]
561→564[p_1|2]
562→563[p_1|1]
563→564[p_1|1]
564→565[s_1|1]
564→637[s_1|2]
564→639[s_1|3]
564→641[s_1|3]
564→645[w_1|3]
565→566[s_1|1]
565→570[v_1|2]
566→567[s_1|1]
566→569[p_1|2]
567→568[p_1|1]
568→569[p_1|1]
569→570[v_1|1]
570→571[s_1|1]
570→575[s_1|2]
571→572[s_1|1]
571→574[p_1|2]
572→573[p_1|1]
573→574[p_1|1]
574→575[s_1|1]
575→576[s_1|1]
576→577[s_1|1]
577→578[s_1|1]
578→579[s_1|1]
579→540[s_1|1]
579→550[s_1|1]
579→626[s_1|1]
579→645[s_1|1]
580→581[s_1|1]
581→582[s_1|1]
582→583[s_1|1]
582→587[0_1|2]
583→584[s_1|1]
583→586[p_1|2]
584→585[p_1|1]
585→586[p_1|1]
586→587[0_1|1]
587→588[s_1|1]
588→589[s_1|1]
588→539[p_1|2]
589→590[p_1|1]
590→539[p_1|1]
591→592[s_1|1]
592→593[s_1|1]
593→594[s_1|1]
594→595[s_1|1]
595→596[s_1|1]
596→597[0_1|1]
596→656[s_1|2]
596→658[s_1|3]
597→598[s_1|1]
597→602[p_1|2]
598→599[s_1|1]
598→601[p_1|2]
599→600[p_1|1]
600→601[p_1|1]
601→602[p_1|1]
602→603[p_1|1]
603→604[p_1|1]
604→605[p_1|1]
605→606[p_1|1]
606→607[p_1|1]
607→608[s_1|1]
607→551[s_1|2]
607→627[s_1|2]
607→646[s_1|2]
608→540[p_1|1]
608→550[p_1|1]
608→626[p_1|1]
608→645[p_1|1]
609→610[p_1|1]
610→611[s_1|1]
611→612[s_1|1]
612→613[s_1|1]
613→614[s_1|1]
614→615[s_1|1]
615→616[s_1|1]
616→617[s_1|1]
617→541[0_1|1]
618→619[p_1|3]
619→620[s_1|3]
619→622[s_1|4]
619→626[w_1|4]
620→621[p_1|3]
621→622[s_1|3]
621→626[w_1|4]
622→623[s_1|3]
622→625[p_1|4]
623→624[p_1|3]
624→625[p_1|3]
625→626[w_1|3]
626→627[s_1|3]
627→628[s_1|3]
628→629[s_1|3]
629→630[s_1|3]
630→631[s_1|3]
631→632[s_1|3]
632→633[s_1|3]
632→570[s_1|4]
633→634[s_1|3]
633→636[p_1|4]
634→635[p_1|3]
635→636[p_1|3]
636→570[s_1|3]
637→638[p_1|2]
638→639[s_1|2]
638→641[s_1|3]
638→645[w_1|3]
639→640[p_1|2]
640→641[s_1|2]
640→645[w_1|3]
641→642[s_1|2]
641→644[p_1|3]
642→643[p_1|2]
643→644[p_1|2]
644→645[w_1|2]
645→646[s_1|2]
646→647[s_1|2]
647→648[s_1|2]
648→649[s_1|2]
649→650[s_1|2]
650→651[s_1|2]
651→652[s_1|2]
651→570[s_1|3]
652→653[s_1|2]
652→655[p_1|3]
653→654[p_1|2]
654→655[p_1|2]
655→570[s_1|2]
656→657[p_1|2]
657→658[s_1|2]
658→659[s_1|2]
659→660[s_1|2]
660→661[s_1|2]
661→662[s_1|2]
662→663[s_1|2]
663→664[s_1|2]
664→602[0_1|2]
664→665[s_1|2]
664→667[s_1|3]
665→666[p_1|2]
666→667[s_1|2]
667→668[s_1|2]
668→669[s_1|2]
669→670[s_1|2]
670→671[s_1|2]
671→672[s_1|2]
672→673[s_1|2]
673→603[0_1|2]
673→674[s_1|2]
673→676[s_1|3]
674→675[p_1|2]
675→676[s_1|2]
676→677[s_1|2]
677→678[s_1|2]
678→679[s_1|2]
679→680[s_1|2]
680→681[s_1|2]
681→682[s_1|2]
682→604[0_1|2]
682→683[s_1|2]
682→685[s_1|3]
683→684[p_1|2]
684→685[s_1|2]
685→686[s_1|2]
686→687[s_1|2]
687→688[s_1|2]
688→689[s_1|2]
689→690[s_1|2]
690→691[s_1|2]
691→605[0_1|2]
691→692[s_1|2]
691→694[s_1|3]
692→693[p_1|2]
693→694[s_1|2]
694→695[s_1|2]
695→696[s_1|2]
696→697[s_1|2]
697→698[s_1|2]
698→699[s_1|2]
699→700[s_1|2]
700→606[0_1|2]
700→701[s_1|2]
700→703[s_1|3]
701→702[p_1|2]
702→703[s_1|2]
703→704[s_1|2]
704→705[s_1|2]
705→706[s_1|2]
706→707[s_1|2]
707→708[s_1|2]
708→709[s_1|2]
709→607[0_1|2]